Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(a, y) → f(y, g(y))
g(a) → b
g(b) → b
Q is empty.
↳ QTRS
↳ AAECC Innermost
Q restricted rewrite system:
The TRS R consists of the following rules:
f(a, y) → f(y, g(y))
g(a) → b
g(b) → b
Q is empty.
We have applied [19,8] to switch to innermost. The TRS R 1 is
g(a) → b
g(b) → b
The TRS R 2 is
f(a, y) → f(y, g(y))
The signature Sigma is {f}
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
f(a, y) → f(y, g(y))
g(a) → b
g(b) → b
The set Q consists of the following terms:
f(a, x0)
g(a)
g(b)
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
F(a, y) → F(y, g(y))
F(a, y) → G(y)
The TRS R consists of the following rules:
f(a, y) → f(y, g(y))
g(a) → b
g(b) → b
The set Q consists of the following terms:
f(a, x0)
g(a)
g(b)
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
F(a, y) → F(y, g(y))
F(a, y) → G(y)
The TRS R consists of the following rules:
f(a, y) → f(y, g(y))
g(a) → b
g(b) → b
The set Q consists of the following terms:
f(a, x0)
g(a)
g(b)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
F(a, y) → F(y, g(y))
The TRS R consists of the following rules:
f(a, y) → f(y, g(y))
g(a) → b
g(b) → b
The set Q consists of the following terms:
f(a, x0)
g(a)
g(b)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
F(a, y) → F(y, g(y))
The TRS R consists of the following rules:
g(a) → b
g(b) → b
The set Q consists of the following terms:
f(a, x0)
g(a)
g(b)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
f(a, x0)
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
F(a, y) → F(y, g(y))
The TRS R consists of the following rules:
g(a) → b
g(b) → b
The set Q consists of the following terms:
g(a)
g(b)
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule F(a, y) → F(y, g(y)) at position [] we obtained the following new rules:
F(a, a) → F(a, b)
F(a, b) → F(b, b)
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
F(a, b) → F(b, b)
F(a, a) → F(a, b)
The TRS R consists of the following rules:
g(a) → b
g(b) → b
The set Q consists of the following terms:
g(a)
g(b)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.